The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

group3(@l) → group3#1(@l)
group3#1(::(@x, @xs)) → group3#2(@xs, @x)
group3#1(nil) → nil
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y)
group3#2(nil, @x) → nil
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs))
group3#3(nil, @x, @y) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys)
zip3#2(nil, @l3, @x, @xs) → nil
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
zip3#3(nil, @x, @xs, @y, @ys) → nil

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

group3(@l) → group3#1(@l)
group3#1(::(@x, @xs)) → group3#2(@xs, @x)
group3#1(nil) → nil
group3#2(::(@y, @ys), @x) → group3#3(@ys, @x, @y)
group3#2(nil, @x) → nil
group3#3(::(@z, @zs), @x, @y) → ::(tuple#3(@x, @y, @z), group3(@zs))
group3#3(nil, @x, @y) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@x, @xs), @l2, @l3) → zip3#2(@l2, @l3, @x, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@y, @ys), @l3, @x, @xs) → zip3#3(@l3, @x, @xs, @y, @ys)
zip3#2(nil, @l3, @x, @xs) → nil
zip3#3(::(@z, @zs), @x, @xs, @y, @ys) → ::(tuple#3(@x, @y, @z), zip3(@xs, @ys, @zs))
zip3#3(nil, @x, @xs, @y, @ys) → nil

S is empty.
Rewrite Strategy: INNERMOST

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
::/0
group3#2/1
group3#3/1
group3#3/2
tuple#3/0
tuple#3/1
tuple#3/2
zip3#2/2
zip3#3/1
zip3#3/3

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

S is empty.
Rewrite Strategy: INNERMOST

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
group3, group3#1, group3#2, group3#3, zip3, zip3#1, zip3#2, zip3#3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3
zip3 = zip3#1
zip3 = zip3#2
zip3 = zip3#3
zip3#1 = zip3#2
zip3#1 = zip3#3
zip3#2 = zip3#3

(8) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
zip3#1, group3, group3#1, group3#2, group3#3, zip3, zip3#2, zip3#3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3
zip3 = zip3#1
zip3 = zip3#2
zip3 = zip3#3
zip3#1 = zip3#2
zip3#1 = zip3#3
zip3#2 = zip3#3

(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

Induction Base:
zip3#1(gen_:::nil2_0(0), gen_:::nil2_0(0), gen_:::nil2_0(0)) →_R^Ω(1)
nil

Induction Step:
zip3#1(gen_:::nil2_0(+(n4_0, 1)), gen_:::nil2_0(+(n4_0, 1)), gen_:::nil2_0(+(n4_0, 1))) →_R^Ω(1)
zip3#2(gen_:::nil2_0(+(n4_0, 1)), gen_:::nil2_0(+(n4_0, 1)), gen_:::nil2_0(n4_0)) →_R^Ω(1)
zip3#3(gen_:::nil2_0(+(1, n4_0)), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) →_R^Ω(1)
::(zip3(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0))) →_R^Ω(1)
::(zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0))) →_IH
::(gen_:::nil2_0(c5_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(10) Complex Obligation (BEST)

(11) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
zip3#2, group3, group3#1, group3#2, group3#3, zip3, zip3#3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3
zip3 = zip3#1
zip3 = zip3#2
zip3 = zip3#3
zip3#1 = zip3#2
zip3#1 = zip3#3
zip3#2 = zip3#3

(12) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol zip3#2.

(13) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
zip3#3, group3, group3#1, group3#2, group3#3, zip3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3
zip3 = zip3#1
zip3 = zip3#2
zip3 = zip3#3
zip3#1 = zip3#2
zip3#1 = zip3#3
zip3#2 = zip3#3

(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol zip3#3.

(15) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
zip3, group3, group3#1, group3#2, group3#3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3
zip3 = zip3#1
zip3 = zip3#2
zip3 = zip3#3
zip3#1 = zip3#2
zip3#1 = zip3#3
zip3#2 = zip3#3

(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol zip3.

(17) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
group3#1, group3, group3#2, group3#3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3

(18) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
group3#1(gen_:::nil2_0(*(3, n929_0))) → gen_:::nil2_0(n929_0), rt ∈ Ω(1 + n929₀)

Induction Base:
group3#1(gen_:::nil2_0(*(3, 0))) →_R^Ω(1)
nil

Induction Step:
group3#1(gen_:::nil2_0(*(3, +(n929_0, 1)))) →_R^Ω(1)
group3#2(gen_:::nil2_0(+(2, *(3, n929_0)))) →_R^Ω(1)
group3#3(gen_:::nil2_0(+(1, *(3, n929_0)))) →_R^Ω(1)
::(group3(gen_:::nil2_0(*(3, n929_0)))) →_R^Ω(1)
::(group3#1(gen_:::nil2_0(*(3, n929_0)))) →_IH
::(gen_:::nil2_0(c930_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(19) Complex Obligation (BEST)

(20) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)
group3#1(gen_:::nil2_0(*(3, n929_0))) → gen_:::nil2_0(n929_0), rt ∈ Ω(1 + n929₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
group3#2, group3, group3#3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol group3#2.

(22) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)
group3#1(gen_:::nil2_0(*(3, n929_0))) → gen_:::nil2_0(n929_0), rt ∈ Ω(1 + n929₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
group3#3, group3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol group3#3.

(24) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)
group3#1(gen_:::nil2_0(*(3, n929_0))) → gen_:::nil2_0(n929_0), rt ∈ Ω(1 + n929₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

The following defined symbols remain to be analysed:
group3

They will be analysed ascendingly in the following order:
group3 = group3#1
group3 = group3#2
group3 = group3#3
group3#1 = group3#2
group3#1 = group3#3
group3#2 = group3#3

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol group3.

(26) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)
group3#1(gen_:::nil2_0(*(3, n929_0))) → gen_:::nil2_0(n929_0), rt ∈ Ω(1 + n929₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

No more defined symbols left to analyse.

(27) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

(28) BOUNDS(n^1, INF)

(29) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)
group3#1(gen_:::nil2_0(*(3, n929_0))) → gen_:::nil2_0(n929_0), rt ∈ Ω(1 + n929₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

No more defined symbols left to analyse.

(30) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

(31) BOUNDS(n^1, INF)

(32) Obligation:

Innermost TRS:
Rules:
group3(@l) → group3#1(@l)
group3#1(::(@xs)) → group3#2(@xs)
group3#1(nil) → nil
group3#2(::(@ys)) → group3#3(@ys)
group3#2(nil) → nil
group3#3(::(@zs)) → ::(group3(@zs))
group3#3(nil) → nil
zip3(@l1, @l2, @l3) → zip3#1(@l1, @l2, @l3)
zip3#1(::(@xs), @l2, @l3) → zip3#2(@l2, @l3, @xs)
zip3#1(nil, @l2, @l3) → nil
zip3#2(::(@ys), @l3, @xs) → zip3#3(@l3, @xs, @ys)
zip3#2(nil, @l3, @xs) → nil
zip3#3(::(@zs), @xs, @ys) → ::(zip3(@xs, @ys, @zs))
zip3#3(nil, @xs, @ys) → nil

Types:
group3 :: :::nil → :::nil
group3#1 :: :::nil → :::nil
:: :: :::nil → :::nil
group3#2 :: :::nil → :::nil
nil :: :::nil
group3#3 :: :::nil → :::nil
zip3 :: :::nil → :::nil → :::nil → :::nil
zip3#1 :: :::nil → :::nil → :::nil → :::nil
zip3#2 :: :::nil → :::nil → :::nil → :::nil
zip3#3 :: :::nil → :::nil → :::nil → :::nil
hole_:::nil1_0 :: :::nil
gen_:::nil2_0 :: Nat → :::nil

Lemmas:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

Generator Equations:
gen_:::nil2_0(0) ⇔ nil
gen_:::nil2_0(+(x, 1)) ⇔ ::(gen_:::nil2_0(x))

No more defined symbols left to analyse.

(33) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
zip3#1(gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0), gen_:::nil2_0(n4_0)) → gen_:::nil2_0(n4_0), rt ∈ Ω(1 + n4₀)

(34) BOUNDS(n^1, INF)